00100	Oct 11, 1971
00200	
00300	Requirements and desiderata for the logic for the Missouri program
00400	and the reasoning program.
00500	
00600	The basic requirement is that the logic shall admit convenient proofs
00700	that  strategies  achieve  goals  when  the facts available are those
00800	generally available to humans in the given situation.  This  includes
00900	facts  about  knowledge,  the  value  ascribed  by  a  person  to  an
01000	expression, etc.
01100	
01200	It presently seems best to make the argument of knowledge or
01300	ascription assertions an expression in some language.  This is
01400	because the alternative seems to be modal logic.  The semantics
01500	of one dimension of modality though well established by Kripke
01600	and maybe improved by Scott seem incredibly murky if we have
01700	to use an number of modalities in the same formalism - indeed,
01800	in the same sentence - e.g. "possibly he knowws he can do x."
01900	Then we have to get around the paradox described by Kaplan and
02000	Montague in "Paradox regained".
02100	
02200	One way of getting around the paradox is to use a partial function
02300	logic like that described in my AI memo 1 or that described by
02400	Bochvar.  In such a logic, not all sentences have truth values;
02500	in particular, the sentences expressing paradoxes don't.
02600	There are rules that guarantee that certain kinds of sentences
02700	have truth values, others are asserted by axioms to have
02800	truth values, and certain of the rules of inference enable us
02900	to go from the definedness of certain sentences to those of others.
03000	The class of sentences with truth values, even if we consider
03100	sentences containing only logical constants will not be 
03200	recursively enumerable.  Otherwise, the logic could be replaced
03300	by a second one whose sentences are just the meaningful sentences
03400	of the first logic.  The situation may be worse in that even the
03500	axiom that every sentence is true, false or undefined may bring
03600	back the paradoxes, but this is not clear.
03700	
03800	It would be tempting to try the Scott logic because this handles
03900	definedness in a good way, but it seems clear we need the quantifiers
04000	Scott lacks.  Scott is rumored to know how to imbed his system in
04100	intuitionistic predicate calculus, but I don't understand why
04200	classical predicate calculus is inadequate, why a Bochvar like
04300	logic won't do, or what the implications are of accepting
04400	intuitionistic logic here; must we accept the whole intuitionistic
04500	dogma about what is or isn't meaningful.  Almost surely we can
04600	use their logic without that.
04700	
04800	It would be interesting to see if a partial logic could be found
04900	meeting even the above requirements.
05000	
05100	Another approach is to keep two valued logic, introduce eval as
05200	a specific function of expressions.  Expressions that we secretly
05300	consider to be meaningless have a conventional value UU, and many
05400	of our axioms will have hypotheses that the certain expressions
05500	referred to have a value other than UU.  Thus we will have a 
05600	weakening of the axioms for truth or knowledge that may avoid
05700	the contradictions.
05800	
05900	The use of expressions and some kind of rule allowing us to
06000	go back and forth between a sentence and the assertion of its
06100	truth may allow us to get the benefits of higher order logic
06200	without the pain.  The price will probably come when we try
06300	to describe the semantics of the system.  Incompleteness will
06400	out somewhere - the point is to let it out where it does the
06500	least harm and conflicts least with intuition.
06600	
06700	Another major requirement for the logic is that it allows
06800	the assertion of the result of a calculation
06900	directly with the proof-checker performing the calculation.
07000	Thus we could directly assert
07050	
07100		value[(CAR (QUOTE (A B)))] = A
07200	
07300	from which one could deduce
07400	
07500		car[(A B)] = A
07600	
07700	perhaps by way of
07800	
07900		value[(EQUAL (CAR (QUOTE (A B))) (QUOTE A))] = T.
08000	
08100	Perhaps this last sentence is the one which can be immediately
08200	asserted or even
08300	
08400		true[(EQUAL (CAR (QUOTE (A B)))(QUOTE A))].
08500	
08600	This last form now seems best.